To tackle the increasing complexity of integrated digital electronic circuits, designers need faster and more accurate methods for verifying the functionality and timing of such circuits, particularly in light of the need for ever-shrinking product development times.
The complexity of designing such circuits is often handled by expressing the design in a high-level hardware description language (HLHDL). The HLHDL description is then converted into a physical circuit specification through processes, well known to those of ordinary skill in the art as “synthesis,” involving translation and optimization. Examples of an HLHDL are:                1. IEEE Standard 1364-2001, for the Verilog Hardware Description Language. The Institute of Electrical and Electronics Engineers, Inc., 345 East 47th Street, New York, N.Y. 10017-2394, USA.        2. IEEE Standard 1076-1993, for the VHDL Hardware Description Language. ISBN: 1559373768, August 1994. The Institute of Electrical and Electronics Engineers, Inc., 345 East 47th Street, New York, N.Y. 10017-2394, USA.        
Once the HLHDL design has been created, it needs to be verified, and such HLHDL design can be referred to as the design under test or the design under verification (referred to herein as a “DUT/DUV”).
An HLHDL description can be verified by simulation at the HLHDL level. In another approach, the HLHDL can be translated into a gate-level description that is then simulated, proven by formal methods or is subject to a hybrid combination of simulation and formal approaches.
Verification of an HLHDL description at relatively high-levels of design abstraction is important since detecting a circuit problem early prevents the expenditure of valuable designer time on achieving an efficient physical implementation for a design which, at a higher level, will not achieve its intended purpose. In addition, simulation of the DUT/DUV can be accomplished much more quickly at higher levels of representation than after the DUT/DUV has been translated into a lower-level, more circuit-oriented implementation. For the formal approach, combinatorial “explosion” is a major problem and therefore applying such methods to higher abstraction levels tends to allow them to address a larger portion of the DUT/DUV.
The verification of HLHDL descriptions has been aided by Hardware Verification Languages (or HVLs). An HVL can be implemented and supported by a test-bench automation (TBA) tool. Among other goals, HVLs can provide programming constructs and capabilities more closely matched to the task of verification of a DUT/DUV than are, for example, the HLHDL of the DUT/DUV itself or software-oriented programming languages (such as C or C++).
HVLs can include a programming mechanism by which to specify declarative constraints on a set of variables. Such declarative constraints can be easier to specify than a procedural approach. Uses of declarative constraints can include the following:                i) declaration of “assertions” that specify properties the DUT/DUV must exhibit in order to be regarded as operating correctly; and        ii) declaration of “assumptions” that specify properties the environment of the DUT/DUV must exhibit.        
A DUT/DUV is typically designed such that correct operation is only assured if its environment satisfies a certain set of assumptions that have been input to the verification system as a model of the environment.
In the context of simulation-based verification, an environment that operates according to a set of assumption constraints can be achieved by solving the assumption constraints during the simulation process. In this case, terms of the assumption constraints whose values can be changed (i.e., are under the control of the environment), to find a solution to the environment's assumption constraints during a particular simulation cycle, are referred to as random variables (or RV's). Terms of the assumption constraints not under control of the environment (e.g., driven by the DUT/DUV) are referred to as state variables (or SV's).
In the context of formal verification, the objective is to exhaustively prove, provided the assumption constraints are not violated, that assertions about the DUT/DUV cannot be violated.
It is known how to automatically implement a verification environment, for testing a DUT/DUV, from declarative combinational assumption constraints (or simply “combinational assumption constraints”).
However, combinational assumption constraints cannot specify a time-ordered behavior for an environment since combinational constraints specify assignment of values solely as a functional (or memory less) response to a current state of the various types of inputs that may be applied to it.
It is also known how to automatically implement declarative combinational or sequential assertion constraints. For verification by either formal methods or simulation, such combinational or sequential constraints can be converted, by logic synthesis tools, into an additional circuit, referred to as a “monitor,” that is connected to the DUT/DUV and that asserts an “assertion error” output if an assertion is violated.
It would be desirable to be able to automatically implement a verification environment, for testing a DUT/DUV, from an input set of assumptions that includes declarative sequential assumption constraints (or simply “sequential assumption constraints”).